As circuits have become more complex, improved methods and tools for designing, modifying, and testing those circuits have been developed. Circuits can include integrated circuits, printed circuit board circuits, and other types of circuits at a system level, sub-system level, or even at a transistor level. Improvements in circuit design include the use of electronic design automation (EDA) software tools to generate schematics of circuit designs between a logic and physical design.
Circuit designers need to test or otherwise verify their circuit designs before actually constructing a circuit from a core circuit design, and utilize a variety of software testing tools and techniques that have been developed for testing circuit designs including simulation and formal verification. While simulation can be very effective, it can become very time consuming and may not be able to exhaustively test complex circuit designs due to the large number of possible test vectors, input bits and state bits used to simulate a given circuit. Formal verification, which is presently preferred by circuit designers over simulation for verifying their circuit designs, uses mathematical techniques to either prove that, under a set of constraints, each property in the set of properties is always correct, or to disprove each property (i.e., provide an example condition, called a counterexample, that demonstrates the property is false). In some cases, where the formal verification tool cannot prove or disprove a given property within a predetermined resource limit (e.g., time or memory), the formal verification tool returns an “unknown” status for the property.
Conventional formal verification tools require CPU-intensive computations to prove or falsify properties of a core circuit design. These CPU-intensive computations are essentially repeated by a formal verification tool for every session in regression mode and/or iterative debugging/verification use cases, where each session involves analyzing a current version of the core circuit design to determine whether the current circuit design version satisfies a set of user-supplied properties. The analysis typically involves applying one or more formal verification engines (search operations) to the current circuit design version in accordance with a selected formal verification search strategy, identifying proof objects or counterexamples that prove/disprove a given property, and generating a session result report that may be utilized by the circuit designers (user) to enter corrective modifications to the core circuit design. Because each property must be proven, disproven or designated as “unknown” during every session, and because an average formal verification session involves proving/disproving a few hundred properties (i.e., at a sub-block level) to several thousand or more properties (i.e., at an SoC level), conventional formal verification techniques are considered expensive in terms of processing time and computing resources.
Traditional caching techniques are utilized in some conventional formal verification tools to reduce processing requirements by way of identifying portions of a core circuit design that do not change from one version to the next, thereby obviating the need to perform the expensive computations for properties whose true/false status is entirely based on the identified portion. That is, if a property is proven/disproven during a first session by way of analyzing a certain portion of the core circuit design, that portion of the core circuit design remains unchanged during a subsequent session, and that the formal test bench, which specifies the set of properties (assertions and constraints) is unchanged, then the property may be presumed proven/disproven based on the results generated by the first session. To identify unchanged circuit design portions, traditional caching techniques use isomorphic graph checks in conjunction with initial hash checks for each circuit design version that are compared at the beginning of each session. However, although these caching techniques may reduce total formal verification processing time when applied to multiple versions of a core circuit design, they require extensive computations that must be performed at the beginning of each session, and require a significant amount of memory space (i.e., on the order of megabytes) to generate and compare isomorphic graphs and associated hash values for each design iteration.
What is needed is a formal verification process that can quickly and efficiently identify properties that were previously proven/disproven during previous FV sessions and are not affected by changes to the IC design and the formal test bench that were entered since the previous FV session.